\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $S$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$), $R$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$),\+
\\[0ex]${\it codes}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it decodes}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$), ${\it Req}$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$), ${\it Ack}$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$).
\-\\[0ex]for\= clients $C$ sends FIFO\+
\\[0ex]from j to i via ($S$[j,i],${\it codes}$)
\\[0ex]receives at i via ($R$[i],${\it decodes}$)  requests ${\it Req}$[j] are acknowledged by ${\it Ack}$[j,i]
\-\\[0ex]$\in$ $\mathbb{P}$
\end{tabbing}